/-
Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Florent Schaffhauser
-/
import Mathlib.Algebra.BigOperators.Group.Finset
import Mathlib.Algebra.Group.Submonoid.Basic
import Mathlib.Algebra.Order.Ring.Defs

/-!
# Sums of squares

We introduce sums of squares in a type `R` endowed with an `[Add R]`, `[Zero R]` and `[Mul R]`
instances. Sums of squares in `R` are defined by an inductive predicate `IsSumSq : R → Prop`:
`0 : R` is a sum of squares and if `S` is a sum of squares, then for all `a : R`, `a * a + S` is a
sum of squares in `R`.

## Main declaration

- The predicate `IsSumSq : R → Prop`, defining the property of being a sum of squares in `R`.

## Auxiliary declarations

- The type `sumSqIn R` : in an additive monoid with multiplication `R`, we introduce the type
`sumSqIn R` as the submonoid of `R` whose carrier is the subset `{S : R | IsSumSq S}`.

## Theorems

- `IsSumSq.add`: if `S1` and `S2` are sums of squares in `R`, then so is `S1 + S2`.
- `IsSumSq.nonneg`: in a linearly ordered semiring `R` with an `[ExistsAddOfLE R]` instance, sums of
squares are non-negative.
- `mem_sumSqIn_of_isSquare`: a square is a sum of squares.
- `AddSubmonoid.closure_isSquare`: the submonoid of `R` generated by the squares in `R` is the set
of sums of squares in `R`.

-/

variable {R : Type*} [Mul R]

/--
In a type `R` with an addition, a zero element and a multiplication, the property of being a sum of
squares is defined by an inductive predicate: `0 : R` is a sum of squares and if `S` is a sum of
squares, then for all `a : R`, `a * a + S` is a sum of squares in `R`.
-/
@[mk_iff]
inductive IsSumSq [Add R] [Zero R] : R → Prop
  | zero                              : IsSumSq 0
  | sq_add (a S : R) (pS : IsSumSq S) : IsSumSq (a * a + S)

@[deprecated (since := "2024-08-09")] alias isSumSq := IsSumSq

/--
If `S1` and `S2` are sums of squares in a semiring `R`, then `S1 + S2` is a sum of squares in `R`.
-/
theorem IsSumSq.add [AddMonoid R] {S1 S2 : R} (p1 : IsSumSq S1)
    (p2 : IsSumSq S2) : IsSumSq (S1 + S2) := by
  induction p1 with
  | zero             => rw [zero_add]; exact p2
  | sq_add a S pS ih => rw [add_assoc]; exact IsSumSq.sq_add a (S + S2) ih

@[deprecated (since := "2024-08-09")] alias isSumSq.add := IsSumSq.add

/-- A finite sum of squares is a sum of squares. -/
theorem isSumSq_sum_mul_self {ι : Type*} [AddCommMonoid R] (s : Finset ι) (f : ι → R) :
    IsSumSq (∑ i ∈ s, f i * f i) := by
  induction s using Finset.cons_induction with
  | empty =>
    simpa only [Finset.sum_empty] using IsSumSq.zero
  | cons i s his h =>
    exact (Finset.sum_cons (β := R) his) ▸ IsSumSq.sq_add (f i) (∑ i ∈ s, f i * f i) h

variable (R) in
/--
In an additive monoid with multiplication `R`, the type `sumSqIn R` is the submonoid of sums of
squares in `R`.
-/
def sumSqIn [AddMonoid R] : AddSubmonoid R where
  carrier   := {S : R | IsSumSq S}
  zero_mem' := IsSumSq.zero
  add_mem'  := IsSumSq.add

@[deprecated (since := "2024-08-09")] alias SumSqIn := sumSqIn

/--
In an additive monoid with multiplication, every square is a sum of squares. By definition, a square
in `R` is a term `x : R` such that `x = y * y` for some `y : R` and in Mathlib this is known as
`IsSquare R` (see Mathlib.Algebra.Group.Even).
-/
theorem mem_sumSqIn_of_isSquare [AddMonoid R] {x : R} (px : IsSquare x) : x ∈ sumSqIn R := by
  rcases px with ⟨y, py⟩
  rw [py, ← AddMonoid.add_zero (y * y)]
  exact IsSumSq.sq_add _ _ IsSumSq.zero

@[deprecated (since := "2024-08-09")] alias SquaresInSumSq := mem_sumSqIn_of_isSquare

/--
In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
sums of squares.
-/
theorem AddSubmonoid.closure_isSquare [AddMonoid R] : closure {x : R | IsSquare x} = sumSqIn R := by
  refine le_antisymm (closure_le.2 (fun x hx ↦ mem_sumSqIn_of_isSquare hx)) (fun x hx ↦ ?_)
  induction hx with
  | zero             => exact zero_mem _
  | sq_add a S _ ih  => exact AddSubmonoid.add_mem _ (subset_closure ⟨a, rfl⟩) ih

@[deprecated (since := "2024-08-09")] alias SquaresAddClosure := AddSubmonoid.closure_isSquare

/--
Let `R` be a linearly ordered semiring in which the property `a ≤ b → ∃ c, a + c = b` holds
(e.g. `R = ℕ`). If `S : R` is a sum of squares in `R`, then `0 ≤ S`. This is used in
`Mathlib.Algebra.Ring.Semireal.Defs` to show that linearly ordered fields are semireal.
-/
theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {S : R}
    (pS : IsSumSq S) : 0 ≤ S := by
  induction pS with
  | zero             => simp only [le_refl]
  | sq_add x S _ ih  => apply add_nonneg ?_ ih; simp only [← pow_two x, sq_nonneg]

@[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg
